\begin{tabbing}
$\forall$\=${\it es}$:ES, $C$, $T$:Type, $S_{1}$, $S_{2}$, ${\it Ack}_{1}$, ${\it Ack}_{2}$:($C$$\rightarrow$$C$$\rightarrow$E$\rightarrow\mathbb{P}$), $R_{1}$, ${\it Req}_{1}$, $R_{2}$, ${\it Req}_{2}$:($C$$\rightarrow$E$\rightarrow\mathbb{P}$),\+
\\[0ex]${\it codes}_{1}$:($j$,$i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $S_{1}$($j$,$i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$),
\\[0ex]${\it codes}_{2}$:($j$,$i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $S_{2}$($j$,$i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$),
\\[0ex]${\it decodes}_{1}$:($i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $R_{1}$($i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$),
\\[0ex]${\it decodes}_{2}$:($i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $R_{2}$($i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$), ${\it dec\_R}_{1}$:($i$:$C$$\rightarrow$$e$:E$\rightarrow$Dec($R_{1}$($i$,$e$))).
\-\\[0ex]($\forall$$i$:$C$, $e$:E. $\neg$($R_{1}$($i$,$e$) \& $R_{2}$($i$,$e$)))
\\[0ex]$\Rightarrow$ \=($\forall$${\it dec\_S}_{1}$:($j$,$i$:$C$$\rightarrow$$e$:E$\rightarrow$Dec($S_{1}$($j$,$i$,$e$))).\+
\\[0ex]($\forall$$j$, ${\it j'}$, $i$:$C$, $e$:E. $\neg$($S_{1}$($j$,$i$,$e$) \& $S_{2}$(${\it j'}$,$i$,$e$)))
\\[0ex]$\Rightarrow$ ($\forall$$i$:$C$, $e$:E. Dec($\exists$$j$:$C$. ($S_{1}$($j$,$i$,$e$))))
\\[0ex]$\Rightarrow$ ($\forall$$i$:$C$, $e$:E. Dec($\exists$$j$:$C$. ($S_{2}$($j$,$i$,$e$))))
\\[0ex]$\Rightarrow$ ($\forall$$i$:$C$, $e$:E. Dec($R_{2}$($i$,$e$)))
\\[0ex]$\Rightarrow$ fo\=r\= clients $C$ sends FIFO\+\+
\\[0ex]from j to i via ($S_{1}$[j,i],${\it codes}_{1}$)
\\[0ex]receives at i via ($R_{1}$[i],${\it decodes}_{1}$)
\-\\[0ex]requests ${\it Req}_{1}$[j] are acknowledged by ${\it Ack}_{1}$[j,i]
\-\\[0ex]$\Rightarrow$ fo\=r\= clients $C$ sends FIFO\+\+
\\[0ex]from j to i via ($S_{2}$[j,i],${\it codes}_{2}$)
\\[0ex]receives at i via ($R_{2}$[i],${\it decodes}_{2}$)
\-\\[0ex]requests ${\it Req}_{2}$[j] are acknowledged by ${\it Ack}_{2}$[j,i]
\-\\[0ex]$\Rightarrow$ switch between fifo+ \=s\=end $S_{1}$($j$,$i$,$e$)\+\+
\\[0ex]request ${\it Req}_{1}$($i$,$e$)
\\[0ex]acknowledge ${\it Ack}_{1}$($j$,$i$,$e$) and
\-\\[0ex]send $S_{2}$($j$,$i$,$e$) request ${\it Req}_{2}$($i$,$e$) acknowledge ${\it Ack}_{2}$($j$,$i$,$e$)
\-\\[0ex]$\Rightarrow$ for\= clients $C$ sends FIFO\+
\\[0ex]from j to i via ($\lambda$$j$,$i$,$e$. ($S_{1}$($j$,$i$,$e$)) $\vee$ ($S_{2}$($j$,$i$,$e$))[j,i],[$S_{1}$? ${\it codes}_{1}$ : ${\it codes}_{2}$])
\\[0ex]receives at i via ($\lambda$$i$,$e$. ($R_{1}$($i$,$e$)) $\vee$ ($R_{2}$($i$,$e$))[i],[$R_{1}$ ? ${\it decodes}_{1}$ : ${\it decodes}_{2}$]))
\-\-
\end{tabbing}